let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty AMI-Struct of IL,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 N be with_non-empty_elements set ; :: thesis: for S being non empty AMI-Struct of IL,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 AMI-Struct of IL,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;

dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then reconsider p = la,lb --> a,b as Element of sproduct the Object-Kind of S by A3, A4, CARD_3:def 9;
dom p = {la,lb} by FUNCT_4:65;
hence la,lb --> a,b is FinPartState of S by FINSET_1:29; :: thesis: verum