let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty COM-Struct of N
for A, B being set
for la, lb being Object of S st ObjectKind la = A & ObjectKind lb = B holds
for a being Element of A
for b being Element of B holds (la,lb) --> (a,b) is FinPartState of S
let S be non empty COM-Struct of N; :: thesis: for A, B being set
for la, lb being Object of S st ObjectKind la = A & ObjectKind lb = B holds
for a being Element of A
for b being Element of B holds (la,lb) --> (a,b) is FinPartState of S
let A, B be set ; :: thesis: for la, lb being Object of S st ObjectKind la = A & ObjectKind lb = B holds
for a being Element of A
for b being Element of B holds (la,lb) --> (a,b) is FinPartState of S
let la, lb be Object of S; :: thesis: ( ObjectKind la = A & ObjectKind lb = B implies for a being Element of A
for b being Element of B holds (la,lb) --> (a,b) is FinPartState of S )
assume that
A1: ObjectKind la = A and
A2: ObjectKind lb = B ; :: thesis: for a being Element of A
for b being Element of B holds (la,lb) --> (a,b) is FinPartState of S
let a be Element of A; :: thesis: for b being Element of B holds (la,lb) --> (a,b) is FinPartState of S
let b be Element of B; :: thesis: (la,lb) --> (a,b) is FinPartState of S
set p = (la,lb) --> (a,b);
A3: dom ((la,lb) --> (a,b)) = {la,lb} by FUNCT_4:65;

A4: now

let x be set ; :: thesis: ( x in dom ((la,lb) --> (a,b)) implies ((la,lb) --> (a,b)) . x in the Object-Kind of S . x )
assume A5: x in dom ((la,lb) --> (a,b)) ; :: thesis: ((la,lb) --> (a,b)) . x in the Object-Kind of S . x

now

per cases ( ( la <> lb & x = la ) or ( la <> lb & x = lb ) or ( la = lb & x = la ) ) by A3, A5, TARSKI:def 2;

suppose A6: ( la <> lb & x = la ) ; :: thesis: ((la,lb) --> (a,b)) . x in the Object-Kind of S . x

then ((la,lb) --> (a,b)) . x = a by FUNCT_4:66;
hence ((la,lb) --> (a,b)) . x in the Object-Kind of S . x by A1, A6; :: thesis: verum

end;

suppose A7: ( la <> lb & x = lb ) ; :: thesis: ((la,lb) --> (a,b)) . x in the Object-Kind of S . x

then ((la,lb) --> (a,b)) . x = b by FUNCT_4:66;
hence ((la,lb) --> (a,b)) . x in the Object-Kind of S . x by A2, A7; :: thesis: verum

end;

suppose A8: ( la = lb & x = la ) ; :: thesis: ((la,lb) --> (a,b)) . x in the Object-Kind of S . x

then (la,lb) --> (a,b) = la .--> b by CQC_LANG:44;
then ((la,lb) --> (a,b)) . x = b by A8, FUNCOP_1:87;
hence ((la,lb) --> (a,b)) . x in the Object-Kind of S . x by A2, A8; :: thesis: verum

end;

end;

end;

hence ((la,lb) --> (a,b)) . x in the Object-Kind of S . x ; :: thesis: verum

end;

reconsider p = (la,lb) --> (a,b) as PartState of S by A4, FUNCT_1:def 20;
dom p = {la,lb} by FUNCT_4:65;
hence (la,lb) --> (a,b) is FinPartState of S ; :: thesis: verum